Problem: 0(x1) -> 1(x1) 0(0(x1)) -> 0(x1) 3(4(5(x1))) -> 4(3(5(x1))) 2(2(2(2(2(2(2(2(2(2(2(2(2(x1))))))))))))) -> 0(0(0(1(0(1(1(1(0(1(1(1(1(0(0(0(0(1(0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(0( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1(1(0(0(1(1(1(1(1(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 1(1(0(0(1(1(0(1(0(0(1(0(1(1(1(1(1(0(0(1(0(1(1(1(0(1(0(0(0(0(1(0(1(1( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1(0(1(1(0(0(0(1(1(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> 2(2(2(2(2(2(2(2(2(2(2(2(2(x1))))))))))))) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {6,5,4,3} transitions: 41(21) -> 22* 31(20) -> 21* 51(19) -> 20* 51(23) -> 24* 11(9) -> 10* 11(11) -> 12* 00(2) -> 3* 00(1) -> 3* 10(2) -> 6* 10(1) -> 6* 30(2) -> 4* 30(1) -> 4* 40(2) -> 1* 40(1) -> 1* 50(2) -> 2* 50(1) -> 2* 20(2) -> 5* 20(1) -> 5* 1 -> 23,9 2 -> 19,11 10 -> 3* 12 -> 3* 22 -> 4* 24 -> 20* problem: Qed